YES 3.315 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



↳ HASKELL
  ↳ LR

mainModule List
  ((elemIndex :: Eq a => Maybe a  ->  [Maybe a]  ->  Maybe Int) :: Eq a => Maybe a  ->  [Maybe a]  ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude
  elemIndex :: Eq a => a  ->  [a]  ->  Maybe Int
elemIndex x = findIndex (== x)

  findIndex :: (a  ->  Bool)  ->  [a]  ->  Maybe Int
findIndex p = Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool)  ->  [a]  ->  [Int]
findIndices p xs = concatMap (\vv1 ->
case vv1 of
  (x,i)->  if p x then i : [] else []
  _-> []
) (zip xs (enumFrom 0))


module Maybe where
  import qualified List
import qualified Prelude
  listToMaybe :: [a]  ->  Maybe a
listToMaybe [] = Nothing
listToMaybe (a : _) = Just a



Lambda Reductions:
The following Lambda expression
\vv1→
case vv1 of
 (x,i) → if p x then i : [] else []
 _ → []

is transformed to
findIndices0 p vv1 = 
case vv1 of
 (x,i) → if p x then i : [] else []
 _ → []

The following Lambda expression
\ab→(a,b)

is transformed to
zip0 a b = (a,b)



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR

mainModule List
  ((elemIndex :: Eq a => Maybe a  ->  [Maybe a]  ->  Maybe Int) :: Eq a => Maybe a  ->  [Maybe a]  ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude
  elemIndex :: Eq a => a  ->  [a]  ->  Maybe Int
elemIndex x = findIndex (== x)

  findIndex :: (a  ->  Bool)  ->  [a]  ->  Maybe Int
findIndex p = Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool)  ->  [a]  ->  [Int]
findIndices p xs = concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 = 
case vv1 of
  (x,i)->  if p x then i : [] else []
  _-> []


module Maybe where
  import qualified List
import qualified Prelude
  listToMaybe :: [a]  ->  Maybe a
listToMaybe [] = Nothing
listToMaybe (a : _) = Just a



Case Reductions:
The following Case expression
case vv1 of
 (x,i) → if p x then i : [] else []
 _ → []

is transformed to
findIndices00 p (x,i) = if p x then i : [] else []
findIndices00 p _ = []



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR

mainModule List
  ((elemIndex :: Eq a => Maybe a  ->  [Maybe a]  ->  Maybe Int) :: Eq a => Maybe a  ->  [Maybe a]  ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude
  elemIndex :: Eq a => a  ->  [a]  ->  Maybe Int
elemIndex x = findIndex (== x)

  findIndex :: (a  ->  Bool)  ->  [a]  ->  Maybe Int
findIndex p = Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool)  ->  [a]  ->  [Int]
findIndices p xs = concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 = findIndices00 p vv1

  
findIndices00 p (x,i) =  if p x then i : [] else []
findIndices00 p _ = []


module Maybe where
  import qualified List
import qualified Prelude
  listToMaybe :: [a]  ->  Maybe a
listToMaybe [] = Nothing
listToMaybe (a : _) = Just a



If Reductions:
The following If expression
if p x then i : [] else []

is transformed to
findIndices000 i True = i : []
findIndices000 i False = []



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR

mainModule List
  ((elemIndex :: Eq a => Maybe a  ->  [Maybe a]  ->  Maybe Int) :: Eq a => Maybe a  ->  [Maybe a]  ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude
  elemIndex :: Eq a => a  ->  [a]  ->  Maybe Int
elemIndex x = findIndex (== x)

  findIndex :: (a  ->  Bool)  ->  [a]  ->  Maybe Int
findIndex p = Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool)  ->  [a]  ->  [Int]
findIndices p xs = concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 = findIndices00 p vv1

  
findIndices00 p (x,i) = findIndices000 i (p x)
findIndices00 p _ = []

  
findIndices000 i True = i : []
findIndices000 i False = []


module Maybe where
  import qualified List
import qualified Prelude
  listToMaybe :: [a]  ->  Maybe a
listToMaybe [] = Nothing
listToMaybe (a : _) = Just a



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR

mainModule List
  ((elemIndex :: Eq a => Maybe a  ->  [Maybe a]  ->  Maybe Int) :: Eq a => Maybe a  ->  [Maybe a]  ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude
  elemIndex :: Eq a => a  ->  [a]  ->  Maybe Int
elemIndex x = findIndex (== x)

  findIndex :: (a  ->  Bool)  ->  [a]  ->  Maybe Int
findIndex p = Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool)  ->  [a]  ->  [Int]
findIndices p xs = concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 = findIndices00 p vv1

  
findIndices00 p (x,i) = findIndices000 i (p x)
findIndices00 p vw = []

  
findIndices000 i True = i : []
findIndices000 i False = []


module Maybe where
  import qualified List
import qualified Prelude
  listToMaybe :: [a]  ->  Maybe a
listToMaybe [] = Nothing
listToMaybe (a : vx) = Just a



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed

mainModule List
  ((elemIndex :: Eq a => Maybe a  ->  [Maybe a]  ->  Maybe Int) :: Eq a => Maybe a  ->  [Maybe a]  ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude
  elemIndex :: Eq a => a  ->  [a]  ->  Maybe Int
elemIndex x = findIndex (== x)

  findIndex :: (a  ->  Bool)  ->  [a]  ->  Maybe Int
findIndex p = Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool)  ->  [a]  ->  [Int]
findIndices p xs = concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 = findIndices00 p vv1

  
findIndices00 p (x,i) = findIndices000 i (p x)
findIndices00 p vw = []

  
findIndices000 i True = i : []
findIndices000 i False = []


module Maybe where
  import qualified List
import qualified Prelude
  listToMaybe :: [a]  ->  Maybe a
listToMaybe [] = Nothing
listToMaybe (a : vx) = Just a



Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow

mainModule List
  (elemIndex :: Eq a => Maybe a  ->  [Maybe a]  ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude
  elemIndex :: Eq a => a  ->  [a]  ->  Maybe Int
elemIndex x = findIndex (== x)

  findIndex :: (a  ->  Bool)  ->  [a]  ->  Maybe Int
findIndex p = Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool)  ->  [a]  ->  [Int]
findIndices p xs = concatMap (findIndices0 p) (zip xs (enumFrom (Pos Zero)))

  
findIndices0 p vv1 = findIndices00 p vv1

  
findIndices00 p (x,i) = findIndices000 i (p x)
findIndices00 p vw = []

  
findIndices000 i True = i : []
findIndices000 i False = []


module Maybe where
  import qualified List
import qualified Prelude
  listToMaybe :: [a]  ->  Maybe a
listToMaybe [] = Nothing
listToMaybe (a : vx) = Just a



Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(yv3000), Succ(yv40000)) → new_primEqNat(yv3000, yv40000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(yv5700), Succ(yv4000000)) → new_primPlusNat(yv5700, yv4000000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(yv30000), Succ(yv400000)) → new_primMulNat(yv30000, Succ(yv400000))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), cd, bd, app(ty_[], ed)) → new_esEs1(yv302, yv4002, ed)
new_esEs0(@2(yv300, yv301), @2(yv4000, yv4001), app(app(ty_Either, ga), gb), fc) → new_esEs3(yv300, yv4000, ga, gb)
new_esEs2(Just(yv300), Just(yv4000), app(app(app(ty_@3, bag), bah), bba)) → new_esEs(yv300, yv4000, bag, bah, bba)
new_esEs(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), app(app(ty_Either, cb), cc), bd, be) → new_esEs3(yv300, yv4000, cb, cc)
new_esEs(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), app(ty_Maybe, ca), bd, be) → new_esEs2(yv300, yv4000, ca)
new_esEs(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), cd, bd, app(ty_Maybe, ee)) → new_esEs2(yv302, yv4002, ee)
new_esEs3(Right(yv300), Right(yv4000), bdb, app(app(ty_Either, beb), bec)) → new_esEs3(yv300, yv4000, beb, bec)
new_esEs(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), cd, app(ty_Maybe, dd), be) → new_esEs2(yv301, yv4001, dd)
new_esEs1(:(yv300, yv301), :(yv4000, yv4001), baf) → new_esEs1(yv301, yv4001, baf)
new_esEs(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), cd, bd, app(app(ty_@2, eb), ec)) → new_esEs0(yv302, yv4002, eb, ec)
new_esEs0(@2(yv300, yv301), @2(yv4000, yv4001), app(ty_[], fg), fc) → new_esEs1(yv300, yv4000, fg)
new_esEs(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), cd, app(ty_[], dc), be) → new_esEs1(yv301, yv4001, dc)
new_esEs1(:(yv300, yv301), :(yv4000, yv4001), app(ty_[], bab)) → new_esEs1(yv300, yv4000, bab)
new_esEs(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), app(app(app(ty_@3, ba), bb), bc), bd, be) → new_esEs(yv300, yv4000, ba, bb, bc)
new_esEs2(Just(yv300), Just(yv4000), app(ty_[], bbd)) → new_esEs1(yv300, yv4000, bbd)
new_esEs0(@2(yv300, yv301), @2(yv4000, yv4001), gc, app(app(ty_Either, hc), hd)) → new_esEs3(yv301, yv4001, hc, hd)
new_esEs2(Just(yv300), Just(yv4000), app(ty_Maybe, bbe)) → new_esEs2(yv300, yv4000, bbe)
new_esEs3(Left(yv300), Left(yv4000), app(app(ty_Either, bch), bda), bcc) → new_esEs3(yv300, yv4000, bch, bda)
new_esEs0(@2(yv300, yv301), @2(yv4000, yv4001), gc, app(app(app(ty_@3, gd), ge), gf)) → new_esEs(yv301, yv4001, gd, ge, gf)
new_esEs(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), app(ty_[], bh), bd, be) → new_esEs1(yv300, yv4000, bh)
new_esEs1(:(yv300, yv301), :(yv4000, yv4001), app(app(ty_Either, bad), bae)) → new_esEs3(yv300, yv4000, bad, bae)
new_esEs0(@2(yv300, yv301), @2(yv4000, yv4001), app(app(app(ty_@3, eh), fa), fb), fc) → new_esEs(yv300, yv4000, eh, fa, fb)
new_esEs3(Right(yv300), Right(yv4000), bdb, app(app(app(ty_@3, bdc), bdd), bde)) → new_esEs(yv300, yv4000, bdc, bdd, bde)
new_esEs3(Left(yv300), Left(yv4000), app(ty_Maybe, bcg), bcc) → new_esEs2(yv300, yv4000, bcg)
new_esEs0(@2(yv300, yv301), @2(yv4000, yv4001), gc, app(ty_Maybe, hb)) → new_esEs2(yv301, yv4001, hb)
new_esEs(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), app(app(ty_@2, bf), bg), bd, be) → new_esEs0(yv300, yv4000, bf, bg)
new_esEs3(Left(yv300), Left(yv4000), app(app(ty_@2, bcd), bce), bcc) → new_esEs0(yv300, yv4000, bcd, bce)
new_esEs(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), cd, app(app(ty_@2, da), db), be) → new_esEs0(yv301, yv4001, da, db)
new_esEs3(Right(yv300), Right(yv4000), bdb, app(app(ty_@2, bdf), bdg)) → new_esEs0(yv300, yv4000, bdf, bdg)
new_esEs3(Right(yv300), Right(yv4000), bdb, app(ty_[], bdh)) → new_esEs1(yv300, yv4000, bdh)
new_esEs0(@2(yv300, yv301), @2(yv4000, yv4001), app(ty_Maybe, fh), fc) → new_esEs2(yv300, yv4000, fh)
new_esEs(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), cd, app(app(app(ty_@3, ce), cf), cg), be) → new_esEs(yv301, yv4001, ce, cf, cg)
new_esEs1(:(yv300, yv301), :(yv4000, yv4001), app(ty_Maybe, bac)) → new_esEs2(yv300, yv4000, bac)
new_esEs1(:(yv300, yv301), :(yv4000, yv4001), app(app(app(ty_@3, he), hf), hg)) → new_esEs(yv300, yv4000, he, hf, hg)
new_esEs0(@2(yv300, yv301), @2(yv4000, yv4001), app(app(ty_@2, fd), ff), fc) → new_esEs0(yv300, yv4000, fd, ff)
new_esEs3(Right(yv300), Right(yv4000), bdb, app(ty_Maybe, bea)) → new_esEs2(yv300, yv4000, bea)
new_esEs0(@2(yv300, yv301), @2(yv4000, yv4001), gc, app(ty_[], ha)) → new_esEs1(yv301, yv4001, ha)
new_esEs(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), cd, app(app(ty_Either, de), df), be) → new_esEs3(yv301, yv4001, de, df)
new_esEs2(Just(yv300), Just(yv4000), app(app(ty_Either, bbf), bbg)) → new_esEs3(yv300, yv4000, bbf, bbg)
new_esEs3(Left(yv300), Left(yv4000), app(ty_[], bcf), bcc) → new_esEs1(yv300, yv4000, bcf)
new_esEs0(@2(yv300, yv301), @2(yv4000, yv4001), gc, app(app(ty_@2, gg), gh)) → new_esEs0(yv301, yv4001, gg, gh)
new_esEs1(:(yv300, yv301), :(yv4000, yv4001), app(app(ty_@2, hh), baa)) → new_esEs0(yv300, yv4000, hh, baa)
new_esEs3(Left(yv300), Left(yv4000), app(app(app(ty_@3, bbh), bca), bcb), bcc) → new_esEs(yv300, yv4000, bbh, bca, bcb)
new_esEs(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), cd, bd, app(app(ty_Either, ef), eg)) → new_esEs3(yv302, yv4002, ef, eg)
new_esEs(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), cd, bd, app(app(app(ty_@3, dg), dh), ea)) → new_esEs(yv302, yv4002, dg, dh, ea)
new_esEs2(Just(yv300), Just(yv4000), app(app(ty_@2, bbb), bbc)) → new_esEs0(yv300, yv4000, bbb, bbc)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_listToMaybe0(yv10, yv1110, yv58, yv1111, yv59, ba) → new_listToMaybe(yv58, new_esEs4(Just(yv10), yv1110, ba), yv10, yv1111, yv59, ba)
new_listToMaybe(yv35, False, yv10, :(yv1110, yv1111), yv36, ba) → new_listToMaybe0(yv10, yv1110, new_primPlusNat0(yv36, Zero), yv1111, new_primPlusNat0(yv36, Zero), ba)

The TRS R consists of the following rules:

new_esEs4(Just(yv300), Just(yv4000), app(ty_Maybe, bea)) → new_esEs4(yv300, yv4000, bea)
new_esEs22(yv301, yv4001, app(app(ty_@2, he), hf)) → new_esEs15(yv301, yv4001, he, hf)
new_esEs4(Just(yv300), Just(yv4000), ty_Char) → new_esEs8(yv300, yv4000)
new_esEs19(Left(yv300), Left(yv4000), ty_Ordering, bac) → new_esEs5(yv300, yv4000)
new_primPlusNat1(Succ(yv5700), Succ(yv4000000)) → Succ(Succ(new_primPlusNat1(yv5700, yv4000000)))
new_esEs23(yv300, yv4000, ty_Float) → new_esEs20(yv300, yv4000)
new_primEqInt(Neg(Succ(yv3000)), Pos(yv4000)) → False
new_primEqInt(Pos(Succ(yv3000)), Neg(yv4000)) → False
new_esEs4(Just(yv300), Nothing, bda) → False
new_esEs4(Nothing, Just(yv4000), bda) → False
new_primEqInt(Neg(Zero), Pos(Succ(yv40000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(yv40000))) → False
new_esEs20(Float(yv300, yv301), Float(yv4000, yv4001)) → new_esEs13(new_sr(yv300, yv4000), new_sr(yv301, yv4001))
new_esEs4(Just(yv300), Just(yv4000), app(ty_Ratio, bde)) → new_esEs14(yv300, yv4000, bde)
new_esEs19(Left(yv300), Left(yv4000), app(app(ty_@2, bah), bba), bac) → new_esEs15(yv300, yv4000, bah, bba)
new_esEs17(:(yv300, yv301), :(yv4000, yv4001), bed) → new_asAs(new_esEs23(yv300, yv4000, bed), new_esEs17(yv301, yv4001, bed))
new_esEs12(yv302, yv4002, app(app(ty_@2, ef), eg)) → new_esEs15(yv302, yv4002, ef, eg)
new_esEs19(Right(yv300), Right(yv4000), bbf, app(ty_Ratio, bcb)) → new_esEs14(yv300, yv4000, bcb)
new_esEs10(yv300, yv4000, ty_@0) → new_esEs18(yv300, yv4000)
new_esEs23(yv300, yv4000, app(ty_[], bfc)) → new_esEs17(yv300, yv4000, bfc)
new_esEs21(yv300, yv4000, app(ty_[], ge)) → new_esEs17(yv300, yv4000, ge)
new_esEs22(yv301, yv4001, ty_Integer) → new_esEs6(yv301, yv4001)
new_primMulNat0(Zero, Zero) → Zero
new_esEs21(yv300, yv4000, ty_@0) → new_esEs18(yv300, yv4000)
new_esEs24(yv300, yv4000, ty_Int) → new_esEs13(yv300, yv4000)
new_esEs19(Left(yv300), Left(yv4000), app(app(ty_Either, bbd), bbe), bac) → new_esEs19(yv300, yv4000, bbd, bbe)
new_esEs15(@2(yv300, yv301), @2(yv4000, yv4001), fd, ff) → new_asAs(new_esEs21(yv300, yv4000, fd), new_esEs22(yv301, yv4001, ff))
new_primPlusNat0(Zero, yv400000) → Succ(yv400000)
new_esEs6(Integer(yv300), Integer(yv4000)) → new_primEqInt(yv300, yv4000)
new_esEs21(yv300, yv4000, app(app(ty_@2, gc), gd)) → new_esEs15(yv300, yv4000, gc, gd)
new_esEs23(yv300, yv4000, app(ty_Maybe, bfd)) → new_esEs4(yv300, yv4000, bfd)
new_sr(Neg(yv3000), Pos(yv40000)) → Neg(new_primMulNat0(yv3000, yv40000))
new_sr(Pos(yv3000), Neg(yv40000)) → Neg(new_primMulNat0(yv3000, yv40000))
new_esEs19(Right(yv300), Right(yv4000), bbf, app(app(ty_@2, bcc), bcd)) → new_esEs15(yv300, yv4000, bcc, bcd)
new_esEs11(yv301, yv4001, ty_Double) → new_esEs16(yv301, yv4001)
new_esEs12(yv302, yv4002, ty_Integer) → new_esEs6(yv302, yv4002)
new_esEs11(yv301, yv4001, app(ty_[], df)) → new_esEs17(yv301, yv4001, df)
new_esEs19(Right(yv300), Right(yv4000), bbf, ty_Float) → new_esEs20(yv300, yv4000)
new_esEs11(yv301, yv4001, app(app(ty_@2, dd), de)) → new_esEs15(yv301, yv4001, dd, de)
new_esEs10(yv300, yv4000, app(app(app(ty_@3, be), bf), bg)) → new_esEs9(yv300, yv4000, be, bf, bg)
new_esEs19(Left(yv300), Left(yv4000), app(app(app(ty_@3, bad), bae), baf), bac) → new_esEs9(yv300, yv4000, bad, bae, baf)
new_esEs22(yv301, yv4001, app(ty_Ratio, hd)) → new_esEs14(yv301, yv4001, hd)
new_esEs21(yv300, yv4000, app(ty_Ratio, gb)) → new_esEs14(yv300, yv4000, gb)
new_esEs19(Left(yv300), Left(yv4000), app(ty_Ratio, bag), bac) → new_esEs14(yv300, yv4000, bag)
new_esEs21(yv300, yv4000, ty_Ordering) → new_esEs5(yv300, yv4000)
new_esEs22(yv301, yv4001, app(app(ty_Either, baa), bab)) → new_esEs19(yv301, yv4001, baa, bab)
new_esEs19(Right(yv300), Right(yv4000), bbf, ty_Int) → new_esEs13(yv300, yv4000)
new_esEs22(yv301, yv4001, ty_Float) → new_esEs20(yv301, yv4001)
new_esEs11(yv301, yv4001, app(app(app(ty_@3, cg), da), db)) → new_esEs9(yv301, yv4001, cg, da, db)
new_esEs12(yv302, yv4002, app(app(app(ty_@3, eb), ec), ed)) → new_esEs9(yv302, yv4002, eb, ec, ed)
new_primEqNat0(Zero, Succ(yv40000)) → False
new_primEqNat0(Succ(yv3000), Zero) → False
new_esEs23(yv300, yv4000, ty_Char) → new_esEs8(yv300, yv4000)
new_esEs10(yv300, yv4000, ty_Char) → new_esEs8(yv300, yv4000)
new_esEs12(yv302, yv4002, ty_Double) → new_esEs16(yv302, yv4002)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs4(Just(yv300), Just(yv4000), app(app(ty_Either, beb), bec)) → new_esEs19(yv300, yv4000, beb, bec)
new_esEs4(Nothing, Nothing, bda) → True
new_esEs19(Right(yv300), Right(yv4000), bbf, app(app(app(ty_@3, bbg), bbh), bca)) → new_esEs9(yv300, yv4000, bbg, bbh, bca)
new_esEs11(yv301, yv4001, ty_Float) → new_esEs20(yv301, yv4001)
new_esEs23(yv300, yv4000, ty_Integer) → new_esEs6(yv300, yv4000)
new_esEs19(Left(yv300), Left(yv4000), ty_@0, bac) → new_esEs18(yv300, yv4000)
new_esEs7(False, False) → True
new_esEs4(Just(yv300), Just(yv4000), ty_Integer) → new_esEs6(yv300, yv4000)
new_esEs22(yv301, yv4001, app(ty_[], hg)) → new_esEs17(yv301, yv4001, hg)
new_esEs10(yv300, yv4000, ty_Bool) → new_esEs7(yv300, yv4000)
new_esEs11(yv301, yv4001, ty_Int) → new_esEs13(yv301, yv4001)
new_esEs12(yv302, yv4002, ty_Bool) → new_esEs7(yv302, yv4002)
new_esEs12(yv302, yv4002, ty_@0) → new_esEs18(yv302, yv4002)
new_esEs12(yv302, yv4002, app(ty_[], eh)) → new_esEs17(yv302, yv4002, eh)
new_esEs11(yv301, yv4001, ty_Bool) → new_esEs7(yv301, yv4001)
new_esEs11(yv301, yv4001, ty_Char) → new_esEs8(yv301, yv4001)
new_esEs25(yv301, yv4001, ty_Integer) → new_esEs6(yv301, yv4001)
new_esEs5(EQ, LT) → False
new_esEs5(LT, EQ) → False
new_esEs12(yv302, yv4002, ty_Float) → new_esEs20(yv302, yv4002)
new_esEs11(yv301, yv4001, ty_Ordering) → new_esEs5(yv301, yv4001)
new_esEs23(yv300, yv4000, ty_Int) → new_esEs13(yv300, yv4000)
new_esEs21(yv300, yv4000, app(ty_Maybe, gf)) → new_esEs4(yv300, yv4000, gf)
new_esEs19(Right(yv300), Right(yv4000), bbf, app(app(ty_Either, bcg), bch)) → new_esEs19(yv300, yv4000, bcg, bch)
new_esEs11(yv301, yv4001, app(ty_Ratio, dc)) → new_esEs14(yv301, yv4001, dc)
new_esEs19(Right(yv300), Right(yv4000), bbf, ty_Integer) → new_esEs6(yv300, yv4000)
new_esEs22(yv301, yv4001, ty_Char) → new_esEs8(yv301, yv4001)
new_sr(Neg(yv3000), Neg(yv40000)) → Pos(new_primMulNat0(yv3000, yv40000))
new_esEs19(Left(yv300), Left(yv4000), ty_Int, bac) → new_esEs13(yv300, yv4000)
new_esEs19(Right(yv300), Right(yv4000), bbf, ty_Bool) → new_esEs7(yv300, yv4000)
new_esEs4(Just(yv300), Just(yv4000), app(app(ty_@2, bdf), bdg)) → new_esEs15(yv300, yv4000, bdf, bdg)
new_esEs12(yv302, yv4002, ty_Ordering) → new_esEs5(yv302, yv4002)
new_esEs19(Left(yv300), Left(yv4000), ty_Char, bac) → new_esEs8(yv300, yv4000)
new_esEs12(yv302, yv4002, app(ty_Maybe, fa)) → new_esEs4(yv302, yv4002, fa)
new_sr(Pos(yv3000), Pos(yv40000)) → Pos(new_primMulNat0(yv3000, yv40000))
new_asAs(False, yv56) → False
new_esEs16(Double(yv300, yv301), Double(yv4000, yv4001)) → new_esEs13(new_sr(yv300, yv4000), new_sr(yv301, yv4001))
new_primEqNat0(Zero, Zero) → True
new_esEs14(:%(yv300, yv301), :%(yv4000, yv4001), bfg) → new_asAs(new_esEs24(yv300, yv4000, bfg), new_esEs25(yv301, yv4001, bfg))
new_primMulNat0(Zero, Succ(yv400000)) → Zero
new_primMulNat0(Succ(yv30000), Zero) → Zero
new_esEs19(Right(yv300), Left(yv4000), bbf, bac) → False
new_esEs19(Left(yv300), Right(yv4000), bbf, bac) → False
new_esEs23(yv300, yv4000, app(app(ty_Either, bfe), bff)) → new_esEs19(yv300, yv4000, bfe, bff)
new_esEs11(yv301, yv4001, app(app(ty_Either, dh), ea)) → new_esEs19(yv301, yv4001, dh, ea)
new_esEs10(yv300, yv4000, app(ty_[], cc)) → new_esEs17(yv300, yv4000, cc)
new_esEs4(Just(yv300), Just(yv4000), app(ty_[], bdh)) → new_esEs17(yv300, yv4000, bdh)
new_esEs12(yv302, yv4002, ty_Int) → new_esEs13(yv302, yv4002)
new_esEs23(yv300, yv4000, ty_Ordering) → new_esEs5(yv300, yv4000)
new_esEs23(yv300, yv4000, ty_Bool) → new_esEs7(yv300, yv4000)
new_esEs19(Right(yv300), Right(yv4000), bbf, app(ty_[], bce)) → new_esEs17(yv300, yv4000, bce)
new_esEs10(yv300, yv4000, ty_Ordering) → new_esEs5(yv300, yv4000)
new_esEs25(yv301, yv4001, ty_Int) → new_esEs13(yv301, yv4001)
new_esEs21(yv300, yv4000, ty_Int) → new_esEs13(yv300, yv4000)
new_esEs23(yv300, yv4000, ty_Double) → new_esEs16(yv300, yv4000)
new_esEs21(yv300, yv4000, ty_Double) → new_esEs16(yv300, yv4000)
new_primPlusNat0(Succ(yv570), yv400000) → Succ(Succ(new_primPlusNat1(yv570, yv400000)))
new_esEs13(yv30, yv400) → new_primEqInt(yv30, yv400)
new_esEs19(Right(yv300), Right(yv4000), bbf, ty_Double) → new_esEs16(yv300, yv4000)
new_esEs5(EQ, EQ) → True
new_esEs4(Just(yv300), Just(yv4000), ty_Double) → new_esEs16(yv300, yv4000)
new_esEs22(yv301, yv4001, ty_Ordering) → new_esEs5(yv301, yv4001)
new_esEs12(yv302, yv4002, app(app(ty_Either, fb), fc)) → new_esEs19(yv302, yv4002, fb, fc)
new_esEs19(Right(yv300), Right(yv4000), bbf, ty_@0) → new_esEs18(yv300, yv4000)
new_esEs4(Just(yv300), Just(yv4000), ty_Int) → new_esEs13(yv300, yv4000)
new_primEqInt(Neg(Succ(yv3000)), Neg(Succ(yv40000))) → new_primEqNat0(yv3000, yv40000)
new_esEs19(Left(yv300), Left(yv4000), app(ty_Maybe, bbc), bac) → new_esEs4(yv300, yv4000, bbc)
new_esEs19(Left(yv300), Left(yv4000), ty_Integer, bac) → new_esEs6(yv300, yv4000)
new_esEs4(Just(yv300), Just(yv4000), app(app(app(ty_@3, bdb), bdc), bdd)) → new_esEs9(yv300, yv4000, bdb, bdc, bdd)
new_esEs19(Right(yv300), Right(yv4000), bbf, ty_Char) → new_esEs8(yv300, yv4000)
new_primPlusNat1(Zero, Succ(yv4000000)) → Succ(yv4000000)
new_primPlusNat1(Succ(yv5700), Zero) → Succ(yv5700)
new_esEs19(Right(yv300), Right(yv4000), bbf, ty_Ordering) → new_esEs5(yv300, yv4000)
new_esEs7(True, True) → True
new_esEs21(yv300, yv4000, ty_Char) → new_esEs8(yv300, yv4000)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs22(yv301, yv4001, ty_@0) → new_esEs18(yv301, yv4001)
new_esEs22(yv301, yv4001, ty_Bool) → new_esEs7(yv301, yv4001)
new_esEs10(yv300, yv4000, ty_Int) → new_esEs13(yv300, yv4000)
new_esEs12(yv302, yv4002, app(ty_Ratio, ee)) → new_esEs14(yv302, yv4002, ee)
new_esEs19(Left(yv300), Left(yv4000), app(ty_[], bbb), bac) → new_esEs17(yv300, yv4000, bbb)
new_primEqInt(Neg(Zero), Neg(Succ(yv40000))) → False
new_primEqInt(Neg(Succ(yv3000)), Neg(Zero)) → False
new_esEs5(GT, GT) → True
new_esEs4(Just(yv300), Just(yv4000), ty_Ordering) → new_esEs5(yv300, yv4000)
new_esEs10(yv300, yv4000, ty_Float) → new_esEs20(yv300, yv4000)
new_esEs10(yv300, yv4000, app(app(ty_Either, ce), cf)) → new_esEs19(yv300, yv4000, ce, cf)
new_esEs7(False, True) → False
new_esEs7(True, False) → False
new_esEs22(yv301, yv4001, ty_Double) → new_esEs16(yv301, yv4001)
new_esEs10(yv300, yv4000, app(ty_Ratio, bh)) → new_esEs14(yv300, yv4000, bh)
new_esEs21(yv300, yv4000, app(app(app(ty_@3, fg), fh), ga)) → new_esEs9(yv300, yv4000, fg, fh, ga)
new_esEs21(yv300, yv4000, ty_Integer) → new_esEs6(yv300, yv4000)
new_esEs21(yv300, yv4000, ty_Bool) → new_esEs7(yv300, yv4000)
new_esEs5(LT, LT) → True
new_esEs9(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), bb, bc, bd) → new_asAs(new_esEs10(yv300, yv4000, bb), new_asAs(new_esEs11(yv301, yv4001, bc), new_esEs12(yv302, yv4002, bd)))
new_primPlusNat1(Zero, Zero) → Zero
new_esEs11(yv301, yv4001, ty_@0) → new_esEs18(yv301, yv4001)
new_esEs4(Just(yv300), Just(yv4000), ty_Float) → new_esEs20(yv300, yv4000)
new_esEs19(Left(yv300), Left(yv4000), ty_Float, bac) → new_esEs20(yv300, yv4000)
new_asAs(True, yv56) → yv56
new_esEs10(yv300, yv4000, ty_Integer) → new_esEs6(yv300, yv4000)
new_primMulNat0(Succ(yv30000), Succ(yv400000)) → new_primPlusNat0(new_primMulNat0(yv30000, Succ(yv400000)), yv400000)
new_esEs21(yv300, yv4000, app(app(ty_Either, gg), gh)) → new_esEs19(yv300, yv4000, gg, gh)
new_esEs22(yv301, yv4001, app(ty_Maybe, hh)) → new_esEs4(yv301, yv4001, hh)
new_primEqInt(Pos(Succ(yv3000)), Pos(Succ(yv40000))) → new_primEqNat0(yv3000, yv40000)
new_esEs11(yv301, yv4001, ty_Integer) → new_esEs6(yv301, yv4001)
new_esEs18(@0, @0) → True
new_esEs17([], [], bed) → True
new_esEs17([], :(yv4000, yv4001), bed) → False
new_esEs17(:(yv300, yv301), [], bed) → False
new_esEs4(Just(yv300), Just(yv4000), ty_Bool) → new_esEs7(yv300, yv4000)
new_esEs21(yv300, yv4000, ty_Float) → new_esEs20(yv300, yv4000)
new_esEs23(yv300, yv4000, app(app(app(ty_@3, bee), bef), beg)) → new_esEs9(yv300, yv4000, bee, bef, beg)
new_esEs8(Char(yv300), Char(yv4000)) → new_primEqNat0(yv300, yv4000)
new_primEqNat0(Succ(yv3000), Succ(yv40000)) → new_primEqNat0(yv3000, yv40000)
new_esEs5(GT, EQ) → False
new_esEs5(GT, LT) → False
new_esEs5(EQ, GT) → False
new_esEs5(LT, GT) → False
new_esEs12(yv302, yv4002, ty_Char) → new_esEs8(yv302, yv4002)
new_esEs23(yv300, yv4000, app(ty_Ratio, beh)) → new_esEs14(yv300, yv4000, beh)
new_esEs10(yv300, yv4000, app(app(ty_@2, ca), cb)) → new_esEs15(yv300, yv4000, ca, cb)
new_esEs24(yv300, yv4000, ty_Integer) → new_esEs6(yv300, yv4000)
new_esEs22(yv301, yv4001, ty_Int) → new_esEs13(yv301, yv4001)
new_esEs19(Left(yv300), Left(yv4000), ty_Double, bac) → new_esEs16(yv300, yv4000)
new_esEs19(Right(yv300), Right(yv4000), bbf, app(ty_Maybe, bcf)) → new_esEs4(yv300, yv4000, bcf)
new_esEs23(yv300, yv4000, app(app(ty_@2, bfa), bfb)) → new_esEs15(yv300, yv4000, bfa, bfb)
new_esEs11(yv301, yv4001, app(ty_Maybe, dg)) → new_esEs4(yv301, yv4001, dg)
new_esEs10(yv300, yv4000, ty_Double) → new_esEs16(yv300, yv4000)
new_primEqInt(Pos(Succ(yv3000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(yv40000))) → False
new_esEs22(yv301, yv4001, app(app(app(ty_@3, ha), hb), hc)) → new_esEs9(yv301, yv4001, ha, hb, hc)
new_esEs4(Just(yv300), Just(yv4000), ty_@0) → new_esEs18(yv300, yv4000)
new_esEs19(Left(yv300), Left(yv4000), ty_Bool, bac) → new_esEs7(yv300, yv4000)
new_esEs10(yv300, yv4000, app(ty_Maybe, cd)) → new_esEs4(yv300, yv4000, cd)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs23(yv300, yv4000, ty_@0) → new_esEs18(yv300, yv4000)

The set Q consists of the following terms:

new_esEs19(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs23(x0, x1, ty_Integer)
new_esEs5(EQ, GT)
new_esEs5(GT, EQ)
new_esEs12(x0, x1, ty_Int)
new_esEs4(Just(x0), Just(x1), app(ty_[], x2))
new_esEs19(Right(x0), Right(x1), x2, ty_Double)
new_esEs19(Left(x0), Left(x1), ty_Int, x2)
new_esEs10(x0, x1, ty_Integer)
new_esEs18(@0, @0)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs19(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs19(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs10(x0, x1, app(ty_Maybe, x2))
new_esEs19(Left(x0), Left(x1), ty_Char, x2)
new_esEs12(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_Ordering)
new_esEs12(x0, x1, app(ty_Ratio, x2))
new_esEs4(Just(x0), Just(x1), ty_Bool)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs7(False, False)
new_esEs19(Right(x0), Right(x1), x2, ty_Float)
new_esEs14(:%(x0, x1), :%(x2, x3), x4)
new_esEs11(x0, x1, ty_Bool)
new_esEs11(x0, x1, ty_Float)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs19(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs4(Just(x0), Just(x1), ty_Char)
new_esEs11(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17([], :(x0, x1), x2)
new_primPlusNat1(Succ(x0), Succ(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs12(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs11(x0, x1, app(ty_Maybe, x2))
new_esEs19(Left(x0), Left(x1), ty_Integer, x2)
new_esEs25(x0, x1, ty_Int)
new_esEs4(Just(x0), Just(x1), app(ty_Maybe, x2))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs21(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_@0)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs19(Left(x0), Left(x1), ty_Double, x2)
new_esEs21(x0, x1, ty_Int)
new_esEs12(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs10(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, ty_@0)
new_esEs5(EQ, LT)
new_esEs5(LT, EQ)
new_esEs7(True, False)
new_esEs7(False, True)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_primPlusNat1(Succ(x0), Zero)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs10(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Float)
new_esEs4(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_primPlusNat0(Succ(x0), x1)
new_esEs11(x0, x1, ty_Ordering)
new_esEs12(x0, x1, ty_Integer)
new_esEs11(x0, x1, app(ty_[], x2))
new_esEs11(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, ty_Bool)
new_esEs10(x0, x1, app(ty_Ratio, x2))
new_esEs19(Left(x0), Right(x1), x2, x3)
new_esEs19(Right(x0), Left(x1), x2, x3)
new_esEs23(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Integer)
new_sr(Pos(x0), Pos(x1))
new_esEs10(x0, x1, ty_Int)
new_primPlusNat0(Zero, x0)
new_esEs19(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs10(x0, x1, ty_Ordering)
new_esEs12(x0, x1, ty_@0)
new_esEs10(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_sr(Neg(x0), Neg(x1))
new_primEqNat0(Zero, Zero)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs4(Just(x0), Just(x1), ty_@0)
new_esEs5(LT, LT)
new_esEs21(x0, x1, ty_Float)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_Double)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs8(Char(x0), Char(x1))
new_esEs19(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_primEqNat0(Zero, Succ(x0))
new_esEs24(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Float)
new_esEs11(x0, x1, ty_Double)
new_esEs23(x0, x1, ty_Int)
new_esEs19(Left(x0), Left(x1), ty_Float, x2)
new_esEs5(GT, GT)
new_primMulNat0(Zero, Zero)
new_esEs10(x0, x1, ty_Double)
new_esEs11(x0, x1, ty_Int)
new_esEs15(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs19(Left(x0), Left(x1), ty_@0, x2)
new_esEs22(x0, x1, ty_Bool)
new_esEs12(x0, x1, ty_Char)
new_esEs19(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs11(x0, x1, ty_Integer)
new_esEs21(x0, x1, ty_Char)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17(:(x0, x1), :(x2, x3), x4)
new_esEs11(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs4(Just(x0), Just(x1), ty_Float)
new_esEs16(Double(x0, x1), Double(x2, x3))
new_esEs11(x0, x1, ty_@0)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs11(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primMulNat0(Zero, Succ(x0))
new_esEs7(True, True)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_asAs(False, x0)
new_esEs4(Just(x0), Just(x1), ty_Int)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs10(x0, x1, ty_Char)
new_esEs22(x0, x1, ty_Double)
new_esEs19(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs4(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Zero, Succ(x0))
new_esEs5(EQ, EQ)
new_esEs19(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs10(x0, x1, app(app(ty_Either, x2), x3))
new_esEs19(Right(x0), Right(x1), x2, ty_Bool)
new_primEqNat0(Succ(x0), Zero)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs4(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs4(Just(x0), Just(x1), ty_Integer)
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_esEs19(Left(x0), Left(x1), ty_Ordering, x2)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs22(x0, x1, ty_Int)
new_esEs12(x0, x1, ty_Ordering)
new_esEs12(x0, x1, app(ty_Maybe, x2))
new_esEs4(Nothing, Just(x0), x1)
new_esEs12(x0, x1, ty_Double)
new_esEs21(x0, x1, ty_Ordering)
new_esEs5(LT, GT)
new_esEs5(GT, LT)
new_esEs19(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs19(Left(x0), Left(x1), ty_Bool, x2)
new_esEs19(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_primPlusNat1(Zero, Zero)
new_esEs4(Nothing, Nothing, x0)
new_esEs12(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, ty_Char)
new_esEs12(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Char)
new_esEs11(x0, x1, ty_Char)
new_esEs12(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(Just(x0), Just(x1), ty_Double)
new_esEs13(x0, x1)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs10(x0, x1, ty_Bool)
new_esEs9(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs19(Right(x0), Right(x1), x2, ty_Integer)
new_esEs17(:(x0, x1), [], x2)
new_esEs4(Just(x0), Nothing, x1)
new_primMulNat0(Succ(x0), Zero)
new_esEs23(x0, x1, ty_Bool)
new_asAs(True, x0)
new_esEs19(Right(x0), Right(x1), x2, ty_@0)
new_esEs23(x0, x1, ty_Double)
new_esEs20(Float(x0, x1), Float(x2, x3))
new_esEs4(Just(x0), Just(x1), ty_Ordering)
new_esEs21(x0, x1, ty_@0)
new_esEs4(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs10(x0, x1, ty_Float)
new_esEs19(Right(x0), Right(x1), x2, ty_Char)
new_esEs19(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs25(x0, x1, ty_Integer)
new_esEs19(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs10(x0, x1, app(app(ty_@2, x2), x3))
new_esEs19(Right(x0), Right(x1), x2, ty_Int)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs6(Integer(x0), Integer(x1))
new_esEs17([], [], x0)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

new_listToMaybe1(yv33, False, :(yv4110, yv4111), yv34, ba) → new_listToMaybe1(new_primPlusNat0(yv34, Zero), new_esEs4(Nothing, yv4110, ba), yv4111, new_primPlusNat0(yv34, Zero), ba)

The TRS R consists of the following rules:

new_esEs4(Just(yv300), Just(yv4000), app(ty_Maybe, bea)) → new_esEs4(yv300, yv4000, bea)
new_esEs22(yv301, yv4001, app(app(ty_@2, he), hf)) → new_esEs15(yv301, yv4001, he, hf)
new_esEs4(Just(yv300), Just(yv4000), ty_Char) → new_esEs8(yv300, yv4000)
new_esEs19(Left(yv300), Left(yv4000), ty_Ordering, bac) → new_esEs5(yv300, yv4000)
new_primPlusNat1(Succ(yv5700), Succ(yv4000000)) → Succ(Succ(new_primPlusNat1(yv5700, yv4000000)))
new_esEs23(yv300, yv4000, ty_Float) → new_esEs20(yv300, yv4000)
new_primEqInt(Neg(Succ(yv3000)), Pos(yv4000)) → False
new_primEqInt(Pos(Succ(yv3000)), Neg(yv4000)) → False
new_esEs4(Just(yv300), Nothing, bda) → False
new_esEs4(Nothing, Just(yv4000), bda) → False
new_primEqInt(Neg(Zero), Pos(Succ(yv40000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(yv40000))) → False
new_esEs20(Float(yv300, yv301), Float(yv4000, yv4001)) → new_esEs13(new_sr(yv300, yv4000), new_sr(yv301, yv4001))
new_esEs4(Just(yv300), Just(yv4000), app(ty_Ratio, bde)) → new_esEs14(yv300, yv4000, bde)
new_esEs19(Left(yv300), Left(yv4000), app(app(ty_@2, bah), bba), bac) → new_esEs15(yv300, yv4000, bah, bba)
new_esEs17(:(yv300, yv301), :(yv4000, yv4001), bed) → new_asAs(new_esEs23(yv300, yv4000, bed), new_esEs17(yv301, yv4001, bed))
new_esEs12(yv302, yv4002, app(app(ty_@2, ef), eg)) → new_esEs15(yv302, yv4002, ef, eg)
new_esEs19(Right(yv300), Right(yv4000), bbf, app(ty_Ratio, bcb)) → new_esEs14(yv300, yv4000, bcb)
new_esEs10(yv300, yv4000, ty_@0) → new_esEs18(yv300, yv4000)
new_esEs23(yv300, yv4000, app(ty_[], bfc)) → new_esEs17(yv300, yv4000, bfc)
new_esEs21(yv300, yv4000, app(ty_[], ge)) → new_esEs17(yv300, yv4000, ge)
new_esEs22(yv301, yv4001, ty_Integer) → new_esEs6(yv301, yv4001)
new_primMulNat0(Zero, Zero) → Zero
new_esEs21(yv300, yv4000, ty_@0) → new_esEs18(yv300, yv4000)
new_esEs24(yv300, yv4000, ty_Int) → new_esEs13(yv300, yv4000)
new_esEs19(Left(yv300), Left(yv4000), app(app(ty_Either, bbd), bbe), bac) → new_esEs19(yv300, yv4000, bbd, bbe)
new_esEs15(@2(yv300, yv301), @2(yv4000, yv4001), fd, ff) → new_asAs(new_esEs21(yv300, yv4000, fd), new_esEs22(yv301, yv4001, ff))
new_primPlusNat0(Zero, yv400000) → Succ(yv400000)
new_esEs6(Integer(yv300), Integer(yv4000)) → new_primEqInt(yv300, yv4000)
new_esEs21(yv300, yv4000, app(app(ty_@2, gc), gd)) → new_esEs15(yv300, yv4000, gc, gd)
new_esEs23(yv300, yv4000, app(ty_Maybe, bfd)) → new_esEs4(yv300, yv4000, bfd)
new_sr(Neg(yv3000), Pos(yv40000)) → Neg(new_primMulNat0(yv3000, yv40000))
new_sr(Pos(yv3000), Neg(yv40000)) → Neg(new_primMulNat0(yv3000, yv40000))
new_esEs19(Right(yv300), Right(yv4000), bbf, app(app(ty_@2, bcc), bcd)) → new_esEs15(yv300, yv4000, bcc, bcd)
new_esEs11(yv301, yv4001, ty_Double) → new_esEs16(yv301, yv4001)
new_esEs12(yv302, yv4002, ty_Integer) → new_esEs6(yv302, yv4002)
new_esEs11(yv301, yv4001, app(ty_[], df)) → new_esEs17(yv301, yv4001, df)
new_esEs19(Right(yv300), Right(yv4000), bbf, ty_Float) → new_esEs20(yv300, yv4000)
new_esEs11(yv301, yv4001, app(app(ty_@2, dd), de)) → new_esEs15(yv301, yv4001, dd, de)
new_esEs10(yv300, yv4000, app(app(app(ty_@3, be), bf), bg)) → new_esEs9(yv300, yv4000, be, bf, bg)
new_esEs19(Left(yv300), Left(yv4000), app(app(app(ty_@3, bad), bae), baf), bac) → new_esEs9(yv300, yv4000, bad, bae, baf)
new_esEs22(yv301, yv4001, app(ty_Ratio, hd)) → new_esEs14(yv301, yv4001, hd)
new_esEs21(yv300, yv4000, app(ty_Ratio, gb)) → new_esEs14(yv300, yv4000, gb)
new_esEs19(Left(yv300), Left(yv4000), app(ty_Ratio, bag), bac) → new_esEs14(yv300, yv4000, bag)
new_esEs21(yv300, yv4000, ty_Ordering) → new_esEs5(yv300, yv4000)
new_esEs22(yv301, yv4001, app(app(ty_Either, baa), bab)) → new_esEs19(yv301, yv4001, baa, bab)
new_esEs19(Right(yv300), Right(yv4000), bbf, ty_Int) → new_esEs13(yv300, yv4000)
new_esEs22(yv301, yv4001, ty_Float) → new_esEs20(yv301, yv4001)
new_esEs11(yv301, yv4001, app(app(app(ty_@3, cg), da), db)) → new_esEs9(yv301, yv4001, cg, da, db)
new_esEs12(yv302, yv4002, app(app(app(ty_@3, eb), ec), ed)) → new_esEs9(yv302, yv4002, eb, ec, ed)
new_primEqNat0(Zero, Succ(yv40000)) → False
new_primEqNat0(Succ(yv3000), Zero) → False
new_esEs23(yv300, yv4000, ty_Char) → new_esEs8(yv300, yv4000)
new_esEs10(yv300, yv4000, ty_Char) → new_esEs8(yv300, yv4000)
new_esEs12(yv302, yv4002, ty_Double) → new_esEs16(yv302, yv4002)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs4(Just(yv300), Just(yv4000), app(app(ty_Either, beb), bec)) → new_esEs19(yv300, yv4000, beb, bec)
new_esEs4(Nothing, Nothing, bda) → True
new_esEs19(Right(yv300), Right(yv4000), bbf, app(app(app(ty_@3, bbg), bbh), bca)) → new_esEs9(yv300, yv4000, bbg, bbh, bca)
new_esEs11(yv301, yv4001, ty_Float) → new_esEs20(yv301, yv4001)
new_esEs23(yv300, yv4000, ty_Integer) → new_esEs6(yv300, yv4000)
new_esEs19(Left(yv300), Left(yv4000), ty_@0, bac) → new_esEs18(yv300, yv4000)
new_esEs7(False, False) → True
new_esEs4(Just(yv300), Just(yv4000), ty_Integer) → new_esEs6(yv300, yv4000)
new_esEs22(yv301, yv4001, app(ty_[], hg)) → new_esEs17(yv301, yv4001, hg)
new_esEs10(yv300, yv4000, ty_Bool) → new_esEs7(yv300, yv4000)
new_esEs11(yv301, yv4001, ty_Int) → new_esEs13(yv301, yv4001)
new_esEs12(yv302, yv4002, ty_Bool) → new_esEs7(yv302, yv4002)
new_esEs12(yv302, yv4002, ty_@0) → new_esEs18(yv302, yv4002)
new_esEs12(yv302, yv4002, app(ty_[], eh)) → new_esEs17(yv302, yv4002, eh)
new_esEs11(yv301, yv4001, ty_Bool) → new_esEs7(yv301, yv4001)
new_esEs11(yv301, yv4001, ty_Char) → new_esEs8(yv301, yv4001)
new_esEs25(yv301, yv4001, ty_Integer) → new_esEs6(yv301, yv4001)
new_esEs5(EQ, LT) → False
new_esEs5(LT, EQ) → False
new_esEs12(yv302, yv4002, ty_Float) → new_esEs20(yv302, yv4002)
new_esEs11(yv301, yv4001, ty_Ordering) → new_esEs5(yv301, yv4001)
new_esEs23(yv300, yv4000, ty_Int) → new_esEs13(yv300, yv4000)
new_esEs21(yv300, yv4000, app(ty_Maybe, gf)) → new_esEs4(yv300, yv4000, gf)
new_esEs19(Right(yv300), Right(yv4000), bbf, app(app(ty_Either, bcg), bch)) → new_esEs19(yv300, yv4000, bcg, bch)
new_esEs11(yv301, yv4001, app(ty_Ratio, dc)) → new_esEs14(yv301, yv4001, dc)
new_esEs19(Right(yv300), Right(yv4000), bbf, ty_Integer) → new_esEs6(yv300, yv4000)
new_esEs22(yv301, yv4001, ty_Char) → new_esEs8(yv301, yv4001)
new_sr(Neg(yv3000), Neg(yv40000)) → Pos(new_primMulNat0(yv3000, yv40000))
new_esEs19(Left(yv300), Left(yv4000), ty_Int, bac) → new_esEs13(yv300, yv4000)
new_esEs19(Right(yv300), Right(yv4000), bbf, ty_Bool) → new_esEs7(yv300, yv4000)
new_esEs4(Just(yv300), Just(yv4000), app(app(ty_@2, bdf), bdg)) → new_esEs15(yv300, yv4000, bdf, bdg)
new_esEs12(yv302, yv4002, ty_Ordering) → new_esEs5(yv302, yv4002)
new_esEs19(Left(yv300), Left(yv4000), ty_Char, bac) → new_esEs8(yv300, yv4000)
new_esEs12(yv302, yv4002, app(ty_Maybe, fa)) → new_esEs4(yv302, yv4002, fa)
new_sr(Pos(yv3000), Pos(yv40000)) → Pos(new_primMulNat0(yv3000, yv40000))
new_asAs(False, yv56) → False
new_esEs16(Double(yv300, yv301), Double(yv4000, yv4001)) → new_esEs13(new_sr(yv300, yv4000), new_sr(yv301, yv4001))
new_primEqNat0(Zero, Zero) → True
new_esEs14(:%(yv300, yv301), :%(yv4000, yv4001), bfg) → new_asAs(new_esEs24(yv300, yv4000, bfg), new_esEs25(yv301, yv4001, bfg))
new_primMulNat0(Zero, Succ(yv400000)) → Zero
new_primMulNat0(Succ(yv30000), Zero) → Zero
new_esEs19(Right(yv300), Left(yv4000), bbf, bac) → False
new_esEs19(Left(yv300), Right(yv4000), bbf, bac) → False
new_esEs23(yv300, yv4000, app(app(ty_Either, bfe), bff)) → new_esEs19(yv300, yv4000, bfe, bff)
new_esEs11(yv301, yv4001, app(app(ty_Either, dh), ea)) → new_esEs19(yv301, yv4001, dh, ea)
new_esEs10(yv300, yv4000, app(ty_[], cc)) → new_esEs17(yv300, yv4000, cc)
new_esEs4(Just(yv300), Just(yv4000), app(ty_[], bdh)) → new_esEs17(yv300, yv4000, bdh)
new_esEs12(yv302, yv4002, ty_Int) → new_esEs13(yv302, yv4002)
new_esEs23(yv300, yv4000, ty_Ordering) → new_esEs5(yv300, yv4000)
new_esEs23(yv300, yv4000, ty_Bool) → new_esEs7(yv300, yv4000)
new_esEs19(Right(yv300), Right(yv4000), bbf, app(ty_[], bce)) → new_esEs17(yv300, yv4000, bce)
new_esEs10(yv300, yv4000, ty_Ordering) → new_esEs5(yv300, yv4000)
new_esEs25(yv301, yv4001, ty_Int) → new_esEs13(yv301, yv4001)
new_esEs21(yv300, yv4000, ty_Int) → new_esEs13(yv300, yv4000)
new_esEs23(yv300, yv4000, ty_Double) → new_esEs16(yv300, yv4000)
new_esEs21(yv300, yv4000, ty_Double) → new_esEs16(yv300, yv4000)
new_primPlusNat0(Succ(yv570), yv400000) → Succ(Succ(new_primPlusNat1(yv570, yv400000)))
new_esEs13(yv30, yv400) → new_primEqInt(yv30, yv400)
new_esEs19(Right(yv300), Right(yv4000), bbf, ty_Double) → new_esEs16(yv300, yv4000)
new_esEs5(EQ, EQ) → True
new_esEs4(Just(yv300), Just(yv4000), ty_Double) → new_esEs16(yv300, yv4000)
new_esEs22(yv301, yv4001, ty_Ordering) → new_esEs5(yv301, yv4001)
new_esEs12(yv302, yv4002, app(app(ty_Either, fb), fc)) → new_esEs19(yv302, yv4002, fb, fc)
new_esEs19(Right(yv300), Right(yv4000), bbf, ty_@0) → new_esEs18(yv300, yv4000)
new_esEs4(Just(yv300), Just(yv4000), ty_Int) → new_esEs13(yv300, yv4000)
new_primEqInt(Neg(Succ(yv3000)), Neg(Succ(yv40000))) → new_primEqNat0(yv3000, yv40000)
new_esEs19(Left(yv300), Left(yv4000), app(ty_Maybe, bbc), bac) → new_esEs4(yv300, yv4000, bbc)
new_esEs19(Left(yv300), Left(yv4000), ty_Integer, bac) → new_esEs6(yv300, yv4000)
new_esEs4(Just(yv300), Just(yv4000), app(app(app(ty_@3, bdb), bdc), bdd)) → new_esEs9(yv300, yv4000, bdb, bdc, bdd)
new_esEs19(Right(yv300), Right(yv4000), bbf, ty_Char) → new_esEs8(yv300, yv4000)
new_primPlusNat1(Zero, Succ(yv4000000)) → Succ(yv4000000)
new_primPlusNat1(Succ(yv5700), Zero) → Succ(yv5700)
new_esEs19(Right(yv300), Right(yv4000), bbf, ty_Ordering) → new_esEs5(yv300, yv4000)
new_esEs7(True, True) → True
new_esEs21(yv300, yv4000, ty_Char) → new_esEs8(yv300, yv4000)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs22(yv301, yv4001, ty_@0) → new_esEs18(yv301, yv4001)
new_esEs22(yv301, yv4001, ty_Bool) → new_esEs7(yv301, yv4001)
new_esEs10(yv300, yv4000, ty_Int) → new_esEs13(yv300, yv4000)
new_esEs12(yv302, yv4002, app(ty_Ratio, ee)) → new_esEs14(yv302, yv4002, ee)
new_esEs19(Left(yv300), Left(yv4000), app(ty_[], bbb), bac) → new_esEs17(yv300, yv4000, bbb)
new_primEqInt(Neg(Zero), Neg(Succ(yv40000))) → False
new_primEqInt(Neg(Succ(yv3000)), Neg(Zero)) → False
new_esEs5(GT, GT) → True
new_esEs4(Just(yv300), Just(yv4000), ty_Ordering) → new_esEs5(yv300, yv4000)
new_esEs10(yv300, yv4000, ty_Float) → new_esEs20(yv300, yv4000)
new_esEs10(yv300, yv4000, app(app(ty_Either, ce), cf)) → new_esEs19(yv300, yv4000, ce, cf)
new_esEs7(False, True) → False
new_esEs7(True, False) → False
new_esEs22(yv301, yv4001, ty_Double) → new_esEs16(yv301, yv4001)
new_esEs10(yv300, yv4000, app(ty_Ratio, bh)) → new_esEs14(yv300, yv4000, bh)
new_esEs21(yv300, yv4000, app(app(app(ty_@3, fg), fh), ga)) → new_esEs9(yv300, yv4000, fg, fh, ga)
new_esEs21(yv300, yv4000, ty_Integer) → new_esEs6(yv300, yv4000)
new_esEs21(yv300, yv4000, ty_Bool) → new_esEs7(yv300, yv4000)
new_esEs5(LT, LT) → True
new_esEs9(@3(yv300, yv301, yv302), @3(yv4000, yv4001, yv4002), bb, bc, bd) → new_asAs(new_esEs10(yv300, yv4000, bb), new_asAs(new_esEs11(yv301, yv4001, bc), new_esEs12(yv302, yv4002, bd)))
new_primPlusNat1(Zero, Zero) → Zero
new_esEs11(yv301, yv4001, ty_@0) → new_esEs18(yv301, yv4001)
new_esEs4(Just(yv300), Just(yv4000), ty_Float) → new_esEs20(yv300, yv4000)
new_esEs19(Left(yv300), Left(yv4000), ty_Float, bac) → new_esEs20(yv300, yv4000)
new_asAs(True, yv56) → yv56
new_esEs10(yv300, yv4000, ty_Integer) → new_esEs6(yv300, yv4000)
new_primMulNat0(Succ(yv30000), Succ(yv400000)) → new_primPlusNat0(new_primMulNat0(yv30000, Succ(yv400000)), yv400000)
new_esEs21(yv300, yv4000, app(app(ty_Either, gg), gh)) → new_esEs19(yv300, yv4000, gg, gh)
new_esEs22(yv301, yv4001, app(ty_Maybe, hh)) → new_esEs4(yv301, yv4001, hh)
new_primEqInt(Pos(Succ(yv3000)), Pos(Succ(yv40000))) → new_primEqNat0(yv3000, yv40000)
new_esEs11(yv301, yv4001, ty_Integer) → new_esEs6(yv301, yv4001)
new_esEs18(@0, @0) → True
new_esEs17([], [], bed) → True
new_esEs17([], :(yv4000, yv4001), bed) → False
new_esEs17(:(yv300, yv301), [], bed) → False
new_esEs4(Just(yv300), Just(yv4000), ty_Bool) → new_esEs7(yv300, yv4000)
new_esEs21(yv300, yv4000, ty_Float) → new_esEs20(yv300, yv4000)
new_esEs23(yv300, yv4000, app(app(app(ty_@3, bee), bef), beg)) → new_esEs9(yv300, yv4000, bee, bef, beg)
new_esEs8(Char(yv300), Char(yv4000)) → new_primEqNat0(yv300, yv4000)
new_primEqNat0(Succ(yv3000), Succ(yv40000)) → new_primEqNat0(yv3000, yv40000)
new_esEs5(GT, EQ) → False
new_esEs5(GT, LT) → False
new_esEs5(EQ, GT) → False
new_esEs5(LT, GT) → False
new_esEs12(yv302, yv4002, ty_Char) → new_esEs8(yv302, yv4002)
new_esEs23(yv300, yv4000, app(ty_Ratio, beh)) → new_esEs14(yv300, yv4000, beh)
new_esEs10(yv300, yv4000, app(app(ty_@2, ca), cb)) → new_esEs15(yv300, yv4000, ca, cb)
new_esEs24(yv300, yv4000, ty_Integer) → new_esEs6(yv300, yv4000)
new_esEs22(yv301, yv4001, ty_Int) → new_esEs13(yv301, yv4001)
new_esEs19(Left(yv300), Left(yv4000), ty_Double, bac) → new_esEs16(yv300, yv4000)
new_esEs19(Right(yv300), Right(yv4000), bbf, app(ty_Maybe, bcf)) → new_esEs4(yv300, yv4000, bcf)
new_esEs23(yv300, yv4000, app(app(ty_@2, bfa), bfb)) → new_esEs15(yv300, yv4000, bfa, bfb)
new_esEs11(yv301, yv4001, app(ty_Maybe, dg)) → new_esEs4(yv301, yv4001, dg)
new_esEs10(yv300, yv4000, ty_Double) → new_esEs16(yv300, yv4000)
new_primEqInt(Pos(Succ(yv3000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(yv40000))) → False
new_esEs22(yv301, yv4001, app(app(app(ty_@3, ha), hb), hc)) → new_esEs9(yv301, yv4001, ha, hb, hc)
new_esEs4(Just(yv300), Just(yv4000), ty_@0) → new_esEs18(yv300, yv4000)
new_esEs19(Left(yv300), Left(yv4000), ty_Bool, bac) → new_esEs7(yv300, yv4000)
new_esEs10(yv300, yv4000, app(ty_Maybe, cd)) → new_esEs4(yv300, yv4000, cd)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs23(yv300, yv4000, ty_@0) → new_esEs18(yv300, yv4000)

The set Q consists of the following terms:

new_esEs19(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs23(x0, x1, ty_Integer)
new_esEs5(EQ, GT)
new_esEs5(GT, EQ)
new_esEs12(x0, x1, ty_Int)
new_esEs4(Just(x0), Just(x1), app(ty_[], x2))
new_esEs19(Right(x0), Right(x1), x2, ty_Double)
new_esEs19(Left(x0), Left(x1), ty_Int, x2)
new_esEs10(x0, x1, ty_Integer)
new_esEs18(@0, @0)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs19(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs19(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs10(x0, x1, app(ty_Maybe, x2))
new_esEs19(Left(x0), Left(x1), ty_Char, x2)
new_esEs12(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_Ordering)
new_esEs12(x0, x1, app(ty_Ratio, x2))
new_esEs4(Just(x0), Just(x1), ty_Bool)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs7(False, False)
new_esEs19(Right(x0), Right(x1), x2, ty_Float)
new_esEs14(:%(x0, x1), :%(x2, x3), x4)
new_esEs11(x0, x1, ty_Bool)
new_esEs11(x0, x1, ty_Float)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs19(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs4(Just(x0), Just(x1), ty_Char)
new_esEs11(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17([], :(x0, x1), x2)
new_primPlusNat1(Succ(x0), Succ(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs12(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs11(x0, x1, app(ty_Maybe, x2))
new_esEs19(Left(x0), Left(x1), ty_Integer, x2)
new_esEs25(x0, x1, ty_Int)
new_esEs4(Just(x0), Just(x1), app(ty_Maybe, x2))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs21(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_@0)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs19(Left(x0), Left(x1), ty_Double, x2)
new_esEs21(x0, x1, ty_Int)
new_esEs12(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs10(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, ty_@0)
new_esEs5(EQ, LT)
new_esEs5(LT, EQ)
new_esEs7(True, False)
new_esEs7(False, True)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_primPlusNat1(Succ(x0), Zero)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs10(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Float)
new_esEs4(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_primPlusNat0(Succ(x0), x1)
new_esEs11(x0, x1, ty_Ordering)
new_esEs12(x0, x1, ty_Integer)
new_esEs11(x0, x1, app(ty_[], x2))
new_esEs11(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, ty_Bool)
new_esEs10(x0, x1, app(ty_Ratio, x2))
new_esEs19(Left(x0), Right(x1), x2, x3)
new_esEs19(Right(x0), Left(x1), x2, x3)
new_esEs23(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Integer)
new_sr(Pos(x0), Pos(x1))
new_esEs10(x0, x1, ty_Int)
new_primPlusNat0(Zero, x0)
new_esEs19(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs10(x0, x1, ty_Ordering)
new_esEs12(x0, x1, ty_@0)
new_esEs10(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_sr(Neg(x0), Neg(x1))
new_primEqNat0(Zero, Zero)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs4(Just(x0), Just(x1), ty_@0)
new_esEs5(LT, LT)
new_esEs21(x0, x1, ty_Float)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_Double)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs8(Char(x0), Char(x1))
new_esEs19(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_primEqNat0(Zero, Succ(x0))
new_esEs24(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Float)
new_esEs11(x0, x1, ty_Double)
new_esEs23(x0, x1, ty_Int)
new_esEs19(Left(x0), Left(x1), ty_Float, x2)
new_esEs5(GT, GT)
new_primMulNat0(Zero, Zero)
new_esEs10(x0, x1, ty_Double)
new_esEs11(x0, x1, ty_Int)
new_esEs15(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs19(Left(x0), Left(x1), ty_@0, x2)
new_esEs22(x0, x1, ty_Bool)
new_esEs12(x0, x1, ty_Char)
new_esEs19(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs11(x0, x1, ty_Integer)
new_esEs21(x0, x1, ty_Char)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17(:(x0, x1), :(x2, x3), x4)
new_esEs11(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs4(Just(x0), Just(x1), ty_Float)
new_esEs16(Double(x0, x1), Double(x2, x3))
new_esEs11(x0, x1, ty_@0)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs11(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primMulNat0(Zero, Succ(x0))
new_esEs7(True, True)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_asAs(False, x0)
new_esEs4(Just(x0), Just(x1), ty_Int)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs10(x0, x1, ty_Char)
new_esEs22(x0, x1, ty_Double)
new_esEs19(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs4(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Zero, Succ(x0))
new_esEs5(EQ, EQ)
new_esEs19(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs10(x0, x1, app(app(ty_Either, x2), x3))
new_esEs19(Right(x0), Right(x1), x2, ty_Bool)
new_primEqNat0(Succ(x0), Zero)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs4(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs4(Just(x0), Just(x1), ty_Integer)
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_esEs19(Left(x0), Left(x1), ty_Ordering, x2)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs22(x0, x1, ty_Int)
new_esEs12(x0, x1, ty_Ordering)
new_esEs12(x0, x1, app(ty_Maybe, x2))
new_esEs4(Nothing, Just(x0), x1)
new_esEs12(x0, x1, ty_Double)
new_esEs21(x0, x1, ty_Ordering)
new_esEs5(LT, GT)
new_esEs5(GT, LT)
new_esEs19(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs19(Left(x0), Left(x1), ty_Bool, x2)
new_esEs19(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_primPlusNat1(Zero, Zero)
new_esEs4(Nothing, Nothing, x0)
new_esEs12(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, ty_Char)
new_esEs12(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Char)
new_esEs11(x0, x1, ty_Char)
new_esEs12(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(Just(x0), Just(x1), ty_Double)
new_esEs13(x0, x1)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs10(x0, x1, ty_Bool)
new_esEs9(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs19(Right(x0), Right(x1), x2, ty_Integer)
new_esEs17(:(x0, x1), [], x2)
new_esEs4(Just(x0), Nothing, x1)
new_primMulNat0(Succ(x0), Zero)
new_esEs23(x0, x1, ty_Bool)
new_asAs(True, x0)
new_esEs19(Right(x0), Right(x1), x2, ty_@0)
new_esEs23(x0, x1, ty_Double)
new_esEs20(Float(x0, x1), Float(x2, x3))
new_esEs4(Just(x0), Just(x1), ty_Ordering)
new_esEs21(x0, x1, ty_@0)
new_esEs4(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs10(x0, x1, ty_Float)
new_esEs19(Right(x0), Right(x1), x2, ty_Char)
new_esEs19(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs25(x0, x1, ty_Integer)
new_esEs19(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs10(x0, x1, app(app(ty_@2, x2), x3))
new_esEs19(Right(x0), Right(x1), x2, ty_Int)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs6(Integer(x0), Integer(x1))
new_esEs17([], [], x0)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ UsableRulesProof
                                  ↳ QDP
                                    ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

new_listToMaybe1(yv33, False, :(yv4110, yv4111), yv34, ba) → new_listToMaybe1(new_primPlusNat0(yv34, Zero), new_esEs4(Nothing, yv4110, ba), yv4111, new_primPlusNat0(yv34, Zero), ba)

The TRS R consists of the following rules:

new_primPlusNat0(Zero, yv400000) → Succ(yv400000)
new_primPlusNat0(Succ(yv570), yv400000) → Succ(Succ(new_primPlusNat1(yv570, yv400000)))
new_esEs4(Nothing, Just(yv4000), bda) → False
new_esEs4(Nothing, Nothing, bda) → True
new_primPlusNat1(Succ(yv5700), Succ(yv4000000)) → Succ(Succ(new_primPlusNat1(yv5700, yv4000000)))
new_primPlusNat1(Zero, Succ(yv4000000)) → Succ(yv4000000)
new_primPlusNat1(Succ(yv5700), Zero) → Succ(yv5700)
new_primPlusNat1(Zero, Zero) → Zero

The set Q consists of the following terms:

new_esEs19(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs23(x0, x1, ty_Integer)
new_esEs5(EQ, GT)
new_esEs5(GT, EQ)
new_esEs12(x0, x1, ty_Int)
new_esEs4(Just(x0), Just(x1), app(ty_[], x2))
new_esEs19(Right(x0), Right(x1), x2, ty_Double)
new_esEs19(Left(x0), Left(x1), ty_Int, x2)
new_esEs10(x0, x1, ty_Integer)
new_esEs18(@0, @0)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs19(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs19(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs10(x0, x1, app(ty_Maybe, x2))
new_esEs19(Left(x0), Left(x1), ty_Char, x2)
new_esEs12(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_Ordering)
new_esEs12(x0, x1, app(ty_Ratio, x2))
new_esEs4(Just(x0), Just(x1), ty_Bool)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs7(False, False)
new_esEs19(Right(x0), Right(x1), x2, ty_Float)
new_esEs14(:%(x0, x1), :%(x2, x3), x4)
new_esEs11(x0, x1, ty_Bool)
new_esEs11(x0, x1, ty_Float)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs19(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs4(Just(x0), Just(x1), ty_Char)
new_esEs11(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17([], :(x0, x1), x2)
new_primPlusNat1(Succ(x0), Succ(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs12(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs11(x0, x1, app(ty_Maybe, x2))
new_esEs19(Left(x0), Left(x1), ty_Integer, x2)
new_esEs25(x0, x1, ty_Int)
new_esEs4(Just(x0), Just(x1), app(ty_Maybe, x2))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs21(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_@0)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs19(Left(x0), Left(x1), ty_Double, x2)
new_esEs21(x0, x1, ty_Int)
new_esEs12(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs10(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, ty_@0)
new_esEs5(EQ, LT)
new_esEs5(LT, EQ)
new_esEs7(True, False)
new_esEs7(False, True)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_primPlusNat1(Succ(x0), Zero)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs10(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Float)
new_esEs4(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_primPlusNat0(Succ(x0), x1)
new_esEs11(x0, x1, ty_Ordering)
new_esEs12(x0, x1, ty_Integer)
new_esEs11(x0, x1, app(ty_[], x2))
new_esEs11(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, ty_Bool)
new_esEs10(x0, x1, app(ty_Ratio, x2))
new_esEs19(Left(x0), Right(x1), x2, x3)
new_esEs19(Right(x0), Left(x1), x2, x3)
new_esEs23(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Integer)
new_sr(Pos(x0), Pos(x1))
new_esEs10(x0, x1, ty_Int)
new_primPlusNat0(Zero, x0)
new_esEs19(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs10(x0, x1, ty_Ordering)
new_esEs12(x0, x1, ty_@0)
new_esEs10(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_sr(Neg(x0), Neg(x1))
new_primEqNat0(Zero, Zero)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs4(Just(x0), Just(x1), ty_@0)
new_esEs5(LT, LT)
new_esEs21(x0, x1, ty_Float)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_Double)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs8(Char(x0), Char(x1))
new_esEs19(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_primEqNat0(Zero, Succ(x0))
new_esEs24(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Float)
new_esEs11(x0, x1, ty_Double)
new_esEs23(x0, x1, ty_Int)
new_esEs19(Left(x0), Left(x1), ty_Float, x2)
new_esEs5(GT, GT)
new_primMulNat0(Zero, Zero)
new_esEs10(x0, x1, ty_Double)
new_esEs11(x0, x1, ty_Int)
new_esEs15(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs19(Left(x0), Left(x1), ty_@0, x2)
new_esEs22(x0, x1, ty_Bool)
new_esEs12(x0, x1, ty_Char)
new_esEs19(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs11(x0, x1, ty_Integer)
new_esEs21(x0, x1, ty_Char)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17(:(x0, x1), :(x2, x3), x4)
new_esEs11(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs4(Just(x0), Just(x1), ty_Float)
new_esEs16(Double(x0, x1), Double(x2, x3))
new_esEs11(x0, x1, ty_@0)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs11(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primMulNat0(Zero, Succ(x0))
new_esEs7(True, True)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_asAs(False, x0)
new_esEs4(Just(x0), Just(x1), ty_Int)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs10(x0, x1, ty_Char)
new_esEs22(x0, x1, ty_Double)
new_esEs19(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs4(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Zero, Succ(x0))
new_esEs5(EQ, EQ)
new_esEs19(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs10(x0, x1, app(app(ty_Either, x2), x3))
new_esEs19(Right(x0), Right(x1), x2, ty_Bool)
new_primEqNat0(Succ(x0), Zero)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs4(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs4(Just(x0), Just(x1), ty_Integer)
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_esEs19(Left(x0), Left(x1), ty_Ordering, x2)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs22(x0, x1, ty_Int)
new_esEs12(x0, x1, ty_Ordering)
new_esEs12(x0, x1, app(ty_Maybe, x2))
new_esEs4(Nothing, Just(x0), x1)
new_esEs12(x0, x1, ty_Double)
new_esEs21(x0, x1, ty_Ordering)
new_esEs5(LT, GT)
new_esEs5(GT, LT)
new_esEs19(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs19(Left(x0), Left(x1), ty_Bool, x2)
new_esEs19(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_primPlusNat1(Zero, Zero)
new_esEs4(Nothing, Nothing, x0)
new_esEs12(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, ty_Char)
new_esEs12(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Char)
new_esEs11(x0, x1, ty_Char)
new_esEs12(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(Just(x0), Just(x1), ty_Double)
new_esEs13(x0, x1)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs10(x0, x1, ty_Bool)
new_esEs9(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs19(Right(x0), Right(x1), x2, ty_Integer)
new_esEs17(:(x0, x1), [], x2)
new_esEs4(Just(x0), Nothing, x1)
new_primMulNat0(Succ(x0), Zero)
new_esEs23(x0, x1, ty_Bool)
new_asAs(True, x0)
new_esEs19(Right(x0), Right(x1), x2, ty_@0)
new_esEs23(x0, x1, ty_Double)
new_esEs20(Float(x0, x1), Float(x2, x3))
new_esEs4(Just(x0), Just(x1), ty_Ordering)
new_esEs21(x0, x1, ty_@0)
new_esEs4(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs10(x0, x1, ty_Float)
new_esEs19(Right(x0), Right(x1), x2, ty_Char)
new_esEs19(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs25(x0, x1, ty_Integer)
new_esEs19(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs10(x0, x1, app(app(ty_@2, x2), x3))
new_esEs19(Right(x0), Right(x1), x2, ty_Int)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs6(Integer(x0), Integer(x1))
new_esEs17([], [], x0)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_esEs19(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs23(x0, x1, ty_Integer)
new_esEs5(EQ, GT)
new_esEs5(GT, EQ)
new_esEs12(x0, x1, ty_Int)
new_esEs19(Right(x0), Right(x1), x2, ty_Double)
new_esEs19(Left(x0), Left(x1), ty_Int, x2)
new_esEs10(x0, x1, ty_Integer)
new_esEs18(@0, @0)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs19(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs19(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs10(x0, x1, app(ty_Maybe, x2))
new_esEs19(Left(x0), Left(x1), ty_Char, x2)
new_esEs12(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_Ordering)
new_esEs12(x0, x1, app(ty_Ratio, x2))
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs7(False, False)
new_esEs19(Right(x0), Right(x1), x2, ty_Float)
new_esEs14(:%(x0, x1), :%(x2, x3), x4)
new_esEs11(x0, x1, ty_Bool)
new_esEs11(x0, x1, ty_Float)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs19(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs11(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17([], :(x0, x1), x2)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs12(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs11(x0, x1, app(ty_Maybe, x2))
new_esEs19(Left(x0), Left(x1), ty_Integer, x2)
new_esEs25(x0, x1, ty_Int)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs21(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_@0)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs19(Left(x0), Left(x1), ty_Double, x2)
new_esEs21(x0, x1, ty_Int)
new_esEs12(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs10(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, ty_@0)
new_esEs5(EQ, LT)
new_esEs5(LT, EQ)
new_esEs7(True, False)
new_esEs7(False, True)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs10(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Float)
new_esEs11(x0, x1, ty_Ordering)
new_esEs12(x0, x1, ty_Integer)
new_esEs11(x0, x1, app(ty_[], x2))
new_esEs11(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, ty_Bool)
new_esEs10(x0, x1, app(ty_Ratio, x2))
new_esEs19(Left(x0), Right(x1), x2, x3)
new_esEs19(Right(x0), Left(x1), x2, x3)
new_esEs23(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Integer)
new_sr(Pos(x0), Pos(x1))
new_esEs10(x0, x1, ty_Int)
new_esEs19(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs10(x0, x1, ty_Ordering)
new_esEs12(x0, x1, ty_@0)
new_esEs10(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_sr(Neg(x0), Neg(x1))
new_primEqNat0(Zero, Zero)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs5(LT, LT)
new_esEs21(x0, x1, ty_Float)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_Double)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs8(Char(x0), Char(x1))
new_esEs19(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_primEqNat0(Zero, Succ(x0))
new_esEs24(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Float)
new_esEs11(x0, x1, ty_Double)
new_esEs23(x0, x1, ty_Int)
new_esEs19(Left(x0), Left(x1), ty_Float, x2)
new_esEs5(GT, GT)
new_primMulNat0(Zero, Zero)
new_esEs10(x0, x1, ty_Double)
new_esEs11(x0, x1, ty_Int)
new_esEs15(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs19(Left(x0), Left(x1), ty_@0, x2)
new_esEs22(x0, x1, ty_Bool)
new_esEs12(x0, x1, ty_Char)
new_esEs19(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs11(x0, x1, ty_Integer)
new_esEs21(x0, x1, ty_Char)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17(:(x0, x1), :(x2, x3), x4)
new_esEs11(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs16(Double(x0, x1), Double(x2, x3))
new_esEs11(x0, x1, ty_@0)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs11(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primMulNat0(Zero, Succ(x0))
new_esEs7(True, True)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_asAs(False, x0)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs10(x0, x1, ty_Char)
new_esEs22(x0, x1, ty_Double)
new_esEs19(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs5(EQ, EQ)
new_esEs19(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs10(x0, x1, app(app(ty_Either, x2), x3))
new_esEs19(Right(x0), Right(x1), x2, ty_Bool)
new_primEqNat0(Succ(x0), Zero)
new_primEqNat0(Succ(x0), Succ(x1))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_esEs19(Left(x0), Left(x1), ty_Ordering, x2)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs22(x0, x1, ty_Int)
new_esEs12(x0, x1, ty_Ordering)
new_esEs12(x0, x1, app(ty_Maybe, x2))
new_esEs12(x0, x1, ty_Double)
new_esEs21(x0, x1, ty_Ordering)
new_esEs5(LT, GT)
new_esEs5(GT, LT)
new_esEs19(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs19(Left(x0), Left(x1), ty_Bool, x2)
new_esEs19(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs12(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, ty_Char)
new_esEs12(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Char)
new_esEs11(x0, x1, ty_Char)
new_esEs12(x0, x1, app(app(ty_Either, x2), x3))
new_esEs13(x0, x1)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs10(x0, x1, ty_Bool)
new_esEs9(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs19(Right(x0), Right(x1), x2, ty_Integer)
new_esEs17(:(x0, x1), [], x2)
new_primMulNat0(Succ(x0), Zero)
new_esEs23(x0, x1, ty_Bool)
new_asAs(True, x0)
new_esEs19(Right(x0), Right(x1), x2, ty_@0)
new_esEs23(x0, x1, ty_Double)
new_esEs20(Float(x0, x1), Float(x2, x3))
new_esEs21(x0, x1, ty_@0)
new_esEs10(x0, x1, ty_Float)
new_esEs19(Right(x0), Right(x1), x2, ty_Char)
new_esEs19(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs25(x0, x1, ty_Integer)
new_esEs19(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs10(x0, x1, app(app(ty_@2, x2), x3))
new_esEs19(Right(x0), Right(x1), x2, ty_Int)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs6(Integer(x0), Integer(x1))
new_esEs17([], [], x0)



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ UsableRulesProof
                                  ↳ QDP
                                    ↳ QReductionProof
                                      ↳ QDP
                                        ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_listToMaybe1(yv33, False, :(yv4110, yv4111), yv34, ba) → new_listToMaybe1(new_primPlusNat0(yv34, Zero), new_esEs4(Nothing, yv4110, ba), yv4111, new_primPlusNat0(yv34, Zero), ba)

The TRS R consists of the following rules:

new_primPlusNat0(Zero, yv400000) → Succ(yv400000)
new_primPlusNat0(Succ(yv570), yv400000) → Succ(Succ(new_primPlusNat1(yv570, yv400000)))
new_esEs4(Nothing, Just(yv4000), bda) → False
new_esEs4(Nothing, Nothing, bda) → True
new_primPlusNat1(Succ(yv5700), Succ(yv4000000)) → Succ(Succ(new_primPlusNat1(yv5700, yv4000000)))
new_primPlusNat1(Zero, Succ(yv4000000)) → Succ(yv4000000)
new_primPlusNat1(Succ(yv5700), Zero) → Succ(yv5700)
new_primPlusNat1(Zero, Zero) → Zero

The set Q consists of the following terms:

new_esEs4(Just(x0), Just(x1), app(ty_[], x2))
new_esEs4(Just(x0), Just(x1), ty_Bool)
new_esEs4(Just(x0), Just(x1), ty_Char)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs4(Just(x0), Just(x1), app(ty_Maybe, x2))
new_primPlusNat1(Succ(x0), Zero)
new_esEs4(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_primPlusNat0(Succ(x0), x1)
new_primPlusNat0(Zero, x0)
new_esEs4(Just(x0), Just(x1), ty_@0)
new_esEs4(Just(x0), Just(x1), ty_Float)
new_esEs4(Just(x0), Just(x1), ty_Int)
new_esEs4(Just(x0), Just(x1), app(ty_Ratio, x2))
new_primPlusNat1(Zero, Succ(x0))
new_esEs4(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs4(Just(x0), Just(x1), ty_Integer)
new_esEs4(Nothing, Just(x0), x1)
new_primPlusNat1(Zero, Zero)
new_esEs4(Nothing, Nothing, x0)
new_esEs4(Just(x0), Just(x1), ty_Double)
new_esEs4(Just(x0), Nothing, x1)
new_esEs4(Just(x0), Just(x1), ty_Ordering)
new_esEs4(Just(x0), Just(x1), app(app(ty_Either, x2), x3))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: